{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Types with Typescript\n",
    "### PPL 2020 https://www.cs.bgu.ac.il/~ppl202\n",
    "\n",
    "This lecture introduces the role of **types** in programming languages in the context of Functional Programming.\n",
    "\n",
    "It leads to the definition of the following concepts:\n",
    "\n",
    "1. Operational semantics of programming languages\n",
    "  * High-level definition of programming language semantics\n",
    "  * Distinguish expressions and values in programming languages\n",
    "  * Define expression types: atomic vs. compound expressions\n",
    "  * Define the evaluation algorithm to map expressions to values\n",
    "2. Types in programming languages\n",
    "  * Define value types: atomic vs compound values\n",
    "  * Define typing errors and type safety\n",
    "  * Distinguish untyped and typed programming languages\n",
    "  * Define static and dynamic type checking\n",
    "3. Types with TypeScript \n",
    "  * Illustrate type checking in TypeScript\n",
    "  * Illustrate the benefits of gradual typing with TypeScript\n",
    "  * Review the type language of TypeScript:\n",
    "    * Primitive types vs. Defined types\n",
    "    * Atomic types vs. Compound types\n",
    "\n",
    "In the next lecture, we will go deeper into complex data types in TypeScript and review:\n",
    "* Compound values, literal constants and serialized values with JSON\n",
    "* Recursive types\n",
    "* Generic types\n",
    "* Function types"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Operational Semantics of Programming Languages\n",
    "\n",
    "This section introduces very briefly the notion of *operational semantics for programming languages*.\n",
    "We will refine this definition in Chapter 2.  This definition will help us define more precisely what\n",
    "is meant by *data types*.\n",
    "\n",
    "### High-level definition of programming languages semantics\n",
    "\n",
    "Semantics is the study of the meaning of languages. The word *meaning* is complex and we must specify what is meant by *meaning of a programming language*.  We adopt here the presentation offered in Chapter 1 of:\n",
    "\n",
    "**Semantics with Applications: A Formal Introduction**\n",
    "_Hanne Riis Nielson, Flemming Nielson_\n",
    "Wiley Professional Computing, Wiley, Second Edition 1999.\n",
    "http://www.cs.kun.nl/~hubbers/courses/sc_1718/materiaal/wiley.pdf\n",
    "\n",
    "A computer language is specified by two main components:\n",
    "* a (formal) syntax ג€“ describing the structure of programs as they are written by programmers \n",
    "* a semantics ג€“ which describes the intended meaning of programs.\n",
    "\n",
    "Various tools manipulate programs (compilers, interpreters, debuggers, IDEs, verification tools).\n",
    "All of these tools must agree upon a formal specification of what is expected when we execute the program.\n",
    "The formal semantics of a programming language provides an unambiguous definition of what the execution should achieve.\n",
    "\n",
    "This formal definition has several uses - among which:\n",
    "* People learning the language can understand what each of the programming language construct is expected to achieve. \n",
    "* Implementers of tools for the language (parsers, compilers, interpreters, debuggers etc) have a formal reference for their tool and a formal definition of its correctness/completeness\n",
    "* 2 different programs in the same language or in different languages can be proved formally as equivalent/non-equivalent\n",
    "\n",
    "Proving that programs are equivalent is necessary for example to prove that a compiler generates assembly code which is equivalent to the source program.\n",
    "Naturally, we want to be able to prove that this equivalence holds for any possible source program. "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Semantic Domain\n",
    "\n",
    "Formal semantics gives rules for translation from one domain (usually the programג€™s syntax) to another formally defined domain.  \n",
    "\n",
    "We adopt the **Operational Semantics** approach which determines that:\n",
    "the meaning of an expression in the programming language is specified by the computation it induces when it is executed on a machine.  The operational semantics of a programming language tells us how to execute the program step by step.\n",
    "When we follow this specification, we record the steps and keep track of the **state** of the computation as steps are executed.\n",
    "The specification determines what is meant by the state and which parts of the state are updated when \n",
    "\n",
    "Take as example an imperative programming language with global variables and assignment to variables.\n",
    "For this language, the semantics specifies that the state of an execution consists of the list of defined variables and their value at each step.\n",
    "\n",
    "The result of the execution of a program according to the semantic specification is a **derivation sequence** which represents the computation history.  Each step in the derivation indicates which part of the program was executed, and the state that was reached as a consequence.\n",
    "\n",
    "In this example, a program is a sequence of assignments:\n",
    "```\n",
    "Initial state: [x:5, y:3, z:7]\n",
    "Program: \"z = x; x = y; y = z;\"\n",
    "\n",
    "Step 1: execute \"z=x;\" \n",
    "    Remaining program: \"x=y; y=z;\"\n",
    "    New state: [x:5; y:3, z:5]\n",
    "Step 2: execute \"x=y;\"\n",
    "    Remaining program: \"y=z;\"\n",
    "    New state: [x:3, y:3, z:5]\n",
    "Step 3: execute \"y=z;\"\n",
    "    Remaining program: \"\"\n",
    "    New state: [x:3, y:5, z:5]\n",
    "```\n",
    "\n",
    "This result is the *history of the computation* - it traces the steps of the execution into *primitive steps*\n",
    "and the successive states of the computation.  \n",
    "\n",
    "Note that it is an **abstraction** - it does not provide all the details of what should happen in a concrete computation on specific hardware. For example, it does not mention registers, translation to machine language, encoding of data types.\n",
    "This computation history is a formal mathematical object which is in the **semantic domain**.\n",
    "\n",
    "The rules of the semantics of the specific programming language indicate how to select a sub-expression to evaluate at each\n",
    "step of the computation, and what are the effects on the state of the computation each time a primitive sub-expression is \n",
    "executed.\n",
    "\n",
    "In summary, the operational semantics of the language maps a program and an initial state to a formal structure -\n",
    "we informally refer to this structure as a *computation history*."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Statements vs. Expressions vs. Values\n",
    "\n",
    "In **imperative programs**, programs are constructed from **statements**.  A statement is a unit of program execution.\n",
    "* **Atomic statements** such as variable assignment or print-statements have a single effect either on the world (screen is updated, disk is updated, information is sent in the network) or on the internal state of the program.\n",
    "* **Compound statements** are built from multiple sub-statements.  For example, an `if-then-else` construct is used to\n",
    "build a compound statement, or a `for-loop` construct.  \n",
    "When a statement is executed, the state of the program is modified.\n",
    "\n",
    "In contrast, in **Funcional Programming** (FP), programs are **expressions**.  Expressions can either be:\n",
    "* **Atomic expressions** - for example, the number expression `-12` or the boolean expression `true` or the variable expression `x`.\n",
    "* **Compound expressions** - which are made up of sub-expressions according to the syntax of the language. For example the expression `12 >= 7` is a compound expression made up of 3 sub-expressions. `(12 === 13) ? -1 : 2` is also a compound expression (called a conditional expression).  \n",
    "\n",
    "In FP, we do not 'execute an expression', but instead we compute its value - a process we call **evaluation**.\n",
    "The *evaluation function* maps expressions to **values**.  \n",
    "\n",
    "The operational semantics of an FP language describes how the evaluation function operates over all possible expressions in the language.  It is defined inductively over the syntactic structure of expressions.\n",
    "\n",
    "In the rest of the course, we will focus on specifying the operational semantics of a functional language."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Types of Expressions\n",
    "\n",
    "The JavaScript language mixes both expressions and statements - it is a multi-paradigm language.\n",
    "This makes it difficult to describe completely its operational semantics in a concise manner.\n",
    "We will completely define a smaller language in Chapter 2 - and only provide an informal description for JavaScript.\n",
    "\n",
    "Intuitively, the types of expressions we consider are:\n",
    "* **Atomic expressions**: number expressions (`1, -12`), string expressions (`\"abc\"`), boolean expressions (`true, false`).\n",
    "* **Compound expressions**: arithmetic expressions `(10 + v) * (w / 5)`, relational expressions (`x === 5`), ternary conditional expression `<condition> ? <expr1> : <expr2>`. \n",
    "* **Variable bindings**: these are expressions of the form `let <var> = <expr1>; <expr2>` which define a block in which the variable `<var>` is defined and bound to the value of `<expr1>` and then evaluate the value of `<expr2>`.\n",
    "* **Function invocation**: of the form `f(<expr1>,...,<exprn>)` \n",
    "* **Function definition**: of the form `(<var1>,...) => <expr>`.\n",
    "\n",
    "The list of these expression types and their structure defines the *syntax of the programming language*.\n",
    "Note that we did not include in this partial description the syntax of *statements* in JavaScript.\n",
    "\n",
    "Expressions are combined recursively to form trees of compound expressions with atomic expressions at the leaves. \n",
    "For example:\n",
    "```\n",
    "let v = 12;\n",
    "  (v >= 7) ? (v * 3) : 9\n",
    "```\n",
    "is a compound expression of type `let`, with 2 sub-expressions - a binding expression `v=12` and a body expression which\n",
    "is a conditional ternary expression; in turn, this sub-expression has 3 sub-expressions."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Types of Values\n",
    "\n",
    "Once an expression is evaluated by applying the *evaluation function*, it becomes a **value**.\n",
    "The *evaluation function* maps expressions to values.\n",
    "\n",
    "As we can distinguish types of expressions, we can also characterize the set of all possible values in an inductive manner - that is, start from **atomic values** and then build up **compound values** which are made up of smaller value parts.\n",
    "\n",
    "This lecture focuses on the characterization of the **domain of values** in JavaScript."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Evaluation of Expressions into Values\n",
    "\n",
    "The operational semantics of an FP language defines the evaluation function.  It determines how a top-level expression (the program) is evaluated into a value.  This definition is inductive. For each syntactic construct, an evaluation rule indicates how the sub-expressions are evaluated - in which order.  At each step of the computation, a sub-expression is evaluated and then substituted by its value in the embedding expression.  \n",
    "\n",
    "There may be a need to describe the state of the computation during this evaluation process - similar to the set of bindings `var:value` we observed above when describing the operational semantics of a very simple imperative language.  But the operations on this state will be quite different from what we observed, as in pure FP languages there is no need to perform variable assignment (because variables are immutable).  \n",
    "\n",
    "The output of the operational semantics is a computation history - but in this chapter we will not describe the computation history - we will only describe the values produced by the evaluation function."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Evaluation Algorithm\n",
    "\n",
    "Consider the complex expression we presented above:\n",
    "```\n",
    "let v = 12;\n",
    "  (v >= 7) ? (v * 3) : 9\n",
    "```\n",
    "The evaluation algorithm consists of the following steps: given an expression $E$\n",
    "1. Identify the toplevel syntactic construct of $E$ - in our case a `let` construct.\n",
    "2. Identify the immediate sub-expressions of $E$ - in our case - the binding construct `v=12` and the body (rest of $E$).\n",
    "3. Perform the specific *evaluation rule* defined for the construct of $E$ - in this case - the *let-evaluation rule* is:\n",
    "   1. Compute the value of the `<expr>` on the right-hand-side of the binding expression - call it `v1`.\n",
    "   2. Add to the state of the computation the binding `{v:v1}`\n",
    "   3. Compute the value of the body sub-expression - call it `v2`.\n",
    "   4. Remove the binding `{v:v1}` from the state of the computation.\n",
    "   5. The value of the overall `let` construct is `v2`.\n",
    "\n",
    "This definition of the evaluation function is **recursive**: in steps 3.A and 3.C - we invoked the evaluation function recursively on sub-expressions of $E$.\n",
    "\n",
    "The evaluation function refers to a *state* which describes the set of known variables at every single step of the computation, and the values to which they are bound.\n",
    "\n",
    "This recursive definition must have a base case to terminate. The base case of the recursion consists of evaluating \n",
    "**atomic expressions** or to invoke **atomic primitive operators or functions**.  For example:\n",
    "* The expression `v` is an atomic expression (it has no sub-expressions); it is an expression of type *variable*.\n",
    "The computation rule for evaluating a variable is to lookup its value in the current state of the computation.\n",
    "In our case, the value of the expression `v` is `12`.\n",
    "* The expression `7` is an atomic expression of type `number`; The computation rule for evaluating a number is to convert the way numbers are written in the language into a number value.\n",
    "* The expression `(v >= 7)` is a compound expression of type `relational operator` with a primitive atomic operator (`>=`); The computation rule for evaluating a relational operator is to (1) evaluate the left side sub-expression (we obtain `12`); (2) evaluate the right-side sub-expression (we obtain `7`); (3) pass the 2 values to the primitive comparison operator which must return a boolean value (in this case `true`)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Reduction of Expressions\n",
    "\n",
    "A useful way to think about the evaluation of complex expressions is in terms of **reduction**.\n",
    "\n",
    "Consider the following example (adopted from http://papl.cs.brown.edu/2019/basic-data-expr.html ):\n",
    "\n",
    "We want to evaluate the following expression, which is a formula for computing the wage of a worker given the number of hours she worked:\n",
    "\n",
    "```\n",
    "let hours=45;\n",
    "  (hours <= 40) ? hours * 10 :\n",
    "  (hours > 40) ? (40 * 10) + ((hours - 40) * 15) :\n",
    "  0\n",
    "```\n",
    "\n",
    "This formula in a more explicit form states that:\n",
    "\n",
    "```if (hours <= 40)\n",
    "      hours * 10  // 10$ per hour for less than 40 hours a week\n",
    "   else if (hours > 40)\n",
    "      (40 * 10) + ((hours - 40) * 15) // 10$/hour up to 40hrs - 15$ above\n",
    "   else\n",
    "       0  // This should not happen.\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "475"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let hours=45;\n",
    "  (hours <= 40) ? hours * 10 :\n",
    "  (hours > 40) ? (40 * 10) + ((hours - 40) * 15) :\n",
    "  0"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Letג€™s now see how this expression is reduced to a value, using a step-by-step process:\n",
    "\n",
    "The first step is to **substitute the `hours` variable** with 45:\n",
    "\n",
    "```\n",
    "  (45 <= 40) ? 45 * 10 :\n",
    "  (45 > 40) ? (40 * 10) + ((45 - 40) * 15) :\n",
    "  0\n",
    "```\n",
    "\n",
    "Next, the conditional part of the `?` expression is evaluated, which in this case is false.\n",
    "\n",
    "```\n",
    "=>  false ? 45 * 10 :\n",
    "    (45 > 40): (40 * 10) + ((45 - 40) * 15) :\n",
    "    0\n",
    "```\n",
    "\n",
    "Since the condition is false, the next branch is tried. Note that at each step, a sub-expression is evaluated and replaced by its value:\n",
    "\n",
    "```\n",
    "=>  false ? 45 * 10 :\n",
    "    true: (40 * 10) + ((45 - 40) * 15) :\n",
    "    0\n",
    "```\n",
    "\n",
    "Since the condition is true, the expression reduces to the body of that branch. After that, itג€™s just arithmetic (but each step is done in a specific order):\n",
    "```\n",
    "=>  (40 * 10) + ((45 - 40) * 15)\n",
    "=>  400 + (5 * 15)\n",
    "=>  475\n",
    "```\n",
    "\n",
    "This style of reduction is the best way to think about the evaluation of complex expressions.\n",
    "It is called a process of **reduction** - because the complex expression is incrementally reduced into a value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Types in Programming Languages\n",
    "\n",
    "In the same way as **expressions** can be atomic or compound and built-up into complex recursive programs,\n",
    "the **values** that are generated by programs can be:\n",
    "* **atomic values**: values which have no \"sub-components\" - such as numbers or booleans.\n",
    "* **compound values**: values which are constructed from sub-values, such as arrays or structures.\n",
    "\n",
    "Compound values can be created in the following manner:\n",
    "* Specified as **constant literal values** in the program; for example the expression `[1,2,3]` denotes in JavaScript an array value containing 3 number components.\n",
    "* Computed by **primitive constructor** functions - for example, the expression `[1].concat([12])` returns a new array value containing 2 number components `[1,12]`.\n",
    "* **Deserialized from strings** that represent compound values according to a value syntax (we will see in the next lecture the example of JSON).\n",
    "\n",
    "**NOTE 1**: the capability to specify compound values as literal constants is a characteristic of dynamic languages such as JavaScript, Scheme or Python.  \n",
    "It is more difficult to *write down compound values* in languages such as Java or C++.\n",
    "We will return to this important distinction later.\n",
    "\n",
    "**NOTE 2**: the distinction that a value is atomic depends on a language design decision: for example, strings in JavaScript are defined to be immutable atomic values.  \n",
    "This is because there is no accessor that can take apart a string into characters and mutate one of these parts in place.  \n",
    "In contrast, in C and C++, strings are mutable compound (non-atomic) values (arrays of characters). \n",
    "There are functions in JavaScript that can compute a sub-string of a string, but these are string constructors - they compute a new string given another string as input, not accessors which give access to a part of an existing compound string.\n",
    "\n",
    "\n",
    "### Typed vs. Untyped Languages\n",
    "\n",
    "As you have noted, JavaScript is an **untyped language** - this means: when we declare variables (using the `let` construct)\n",
    "or functions (with the `function` or `=>` constructs), we do not specify the type of the variables or parameters.\n",
    "We also do not need to specify the type returned by the function.\n",
    "\n",
    "This is in contrast to **typed languages** such as Java and C++ - which require the programmer to specify the type\n",
    "of all variables before they can be defined or used.\n",
    "\n",
    "Yet - even if **variables** are not declared with a type in Javascript, **values** in JavaScript **do have** a type -- they can be either `number` or `string` or `boolean` or compound values.\n",
    "\n",
    "Why would we want or not want to declare the type of variables? \n",
    "\n",
    "What are the benefits of each of the approaches?\n",
    "\n",
    "\n",
    "### Typing Errors at Runtime\n",
    "\n",
    "In the description of the evaluation function above, we indicated that expressions are traversed recursively, til \n",
    "atomic expressions are evaluated (into numbers, booleans or strings) and primitive operators or functions are invoked\n",
    "(for example `(v >= 7)`).  \n",
    "\n",
    "When primitive operators or functions are invoked - we can obtain errors at runtime because the value which is passed to the operator does not fit the type of the primitive operator.  \n",
    "For example, in most languages, the evaluation of `(7 >= \"a\")` or `(8 + \"b\")`would return an error at runtime because the \n",
    "operators `\">=\"` and `+` do not know how to operate on a mixture of numbers and strings.\n",
    "This will be the case in Scheme for example as we will see in Chapter 2.\n",
    "\n",
    "#### JavaScript Primitives do not Fail\n",
    "\n",
    "In JavaScript, the language designers took a different approach: they made the primitive operators extremely flexible and robust.  So that evaluations of *strange expressions* do not trigger a runtime error - but instead do either automatic conversions or return special values indicating an *impossible value*.\n",
    "\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "false"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "\"a\" > 2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'2ab'"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "2 + \"ab\""
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "NaN"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "\"a\" * 2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`NaN` is a special value which means *\"Not a Number\"*."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "\"a\" && true"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Non-boolean values are interpreted as boolean when they appear as arguments to boolean operators such as `&&` and `||`.\n",
    "Arithmetic operations are defined over strings and numbers.\n",
    "\n",
    "So that overall - primitive operations in JavaScript do not fail easily.\n",
    "\n",
    "This is a dubious decision - as such automatic handling of unexpected variations is most often a sign of poorly written code\n",
    "and produces *surprising* results."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Accessors to Compound Values in JavaScript do not Fail\n",
    "\n",
    "Another decision of the JavaScript designers was to make access to compound values \"robust\" against runtime errors as well:\n",
    "* Accessing an index out of bounds in an array returns the special value `undefined`\n",
    "* Accessing an undefined key in a map returns the special value `undefined` as well."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let arr=[1];\n",
    "    arr[4]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let map={a:1, b:2}\n",
    "    map.c"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### Undefined Variables in JavaScript do Fail\n",
    "\n",
    "Variables access, however, **can fail**: trying to access an undefined variable raises an error at runtime.\n",
    "When variable expressions are evaluated, it may turn out that the variable is not defined in the current state of the program at the time its value is looked up.  \n",
    "\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "ename": "ReferenceError",
     "evalue": "c is not defined",
     "output_type": "error",
     "traceback": [
      "evalmachine.<anonymous>:2",
      "c; // Trigger a reference error",
      "^",
      "",
      "ReferenceError: c is not defined",
      "    at evalmachine.<anonymous>:2:1",
      "    at ContextifyScript.Script.runInThisContext (vm.js:50:33)",
      "    at Object.runInThisContext (vm.js:139:38)",
      "    at run ([eval]:1002:15)",
      "    at onRunRequest ([eval]:829:18)",
      "    at onMessage ([eval]:789:13)",
      "    at emitTwo (events.js:126:13)",
      "    at process.emit (events.js:214:7)",
      "    at emit (internal/child_process.js:772:12)",
      "    at _combinedTickCallback (internal/process/next_tick.js:141:11)"
     ]
    }
   ],
   "source": [
    "let b=2;\n",
    "    c; // Trigger a reference error"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Similarly, trying to access a key from an `undefined` value triggers an error at runtime:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "ename": "ReferenceError",
     "evalue": "e is not defined",
     "output_type": "error",
     "traceback": [
      "evalmachine.<anonymous>:1",
      "e.k; // e is undefined - triggers an error",
      "^",
      "",
      "ReferenceError: e is not defined",
      "    at evalmachine.<anonymous>:1:1",
      "    at ContextifyScript.Script.runInThisContext (vm.js:50:33)",
      "    at Object.runInThisContext (vm.js:139:38)",
      "    at run ([eval]:1002:15)",
      "    at onRunRequest ([eval]:829:18)",
      "    at onMessage ([eval]:789:13)",
      "    at emitTwo (events.js:126:13)",
      "    at process.emit (events.js:214:7)",
      "    at emit (internal/child_process.js:772:12)",
      "    at _combinedTickCallback (internal/process/next_tick.js:141:11)"
     ]
    }
   ],
   "source": [
    "e.k // e is undefined - triggers an error"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Safety\n",
    "\n",
    "Now that we have seen which errors can be triggered when executing a JavaScript program - and which *surprising* results may be returned when we combine unexpected value types in primitive operators invocations - we return to our question:\n",
    "* Can we avoid such errors and surprises?\n",
    "* What are the benefits of declaring the types of variables?\n",
    "\n",
    "**Type safety** (see https://en.wikipedia.org/wiki/Type_safety) is *the extent to which a programming language discourages or prevents type errors. A type error is erroneous or undesirable program behaviour caused by a discrepancy between differing data types for the program's constants, variables, and methods (functions), e.g., treating an integer (int) as a floating-point number (float).*\n",
    "\n",
    "Type enforcement can be either:\n",
    "* **static**, catching potential errors at compile time, \n",
    "* or **dynamic**, associating type information with values at run-time and consulting them as needed to detect imminent errors,\n",
    "* or a combination of both.\n",
    "\n",
    "In the context of static (compile-time) type systems, type safety usually involves a **guarantee that the eventual value of any expression will be a legitimate member of that expression's static type**.\n",
    "\n",
    "We will develop the notion of type safety incrementally, after we discuss what are types."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Types of Values\n",
    "\n",
    "A data type is a classification of data which indicates what the programmer intends to do with the data. \n",
    "Data types are defined along 2 aspects:\n",
    "* Types correspond to **sets of values** - for example, the type `Boolean` is the set of values {`true`, `false`};\n",
    "  the type `Number` is the (possibly infinite) set of numeric values.\n",
    "* Types define the **operations that can be done on data values** in the set.  For example, values of type `Boolean` can be\n",
    "  computed using logical operators such as `and`, `or`; `Number` values can be manipulated with operators `+`, `*` and\n",
    "  compared with operators such as `<`, `>`.\n",
    "  \n",
    "Types also determine how the interpreter reads and writes the values, and how it stores the values in memory. \n",
    "\n",
    "When discussing types, we must distinguish the **type of a value** and the **type of a variable**:\n",
    "* **Values** always have a type - that is, they belong to a specific set of values. The number `3` belongs to the set of `number` values; the value `true` belongs to the set of `boolean` values.\n",
    "* **Variables** are parts of the programming language expressions. They are bound to values as the expressions are computed at runtime.  When a programmer declares that a *variable has a type* - the meaning is that we express the intent of the programmer that this variable can **only be bound to values of this type** during the lifecycle of the variable. It states a constraint on the variable usage.  \n",
    "\n",
    "In most typed languages, this constraint can be checked at compile time: this is an extremely strong result.  It means that the compiler can at compile time guarantee that all possible executions of the program, with all possible input values will satisfy the stated constraint.  This static verification (that is, a verification performed at compile-time - without knowing the value of the variables) is called **type checking**."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Value Types\n",
    "\n",
    "As mentioned, a value always has a type - this simply states that a value belongs to a set of values.\n",
    "For example, the value `1` belongs to the set of values `number` - which means that the value `1` has type `number`.\n",
    "\n",
    "In most cases, a value will have more than one type: consider for example the case of *sub-types*\n",
    "such as `Integer` and `Number`. `Integer` as a set of values is a proper subset of `Number` as a set of values.\n",
    "This means in particular that a value like `6` belongs both to the type `Integer` and to the type `Number`.\n",
    "\n",
    "A good type system helps programmers not only declare the intended types of variables to obtain type safety,\n",
    "it also helps the programmer **design the range of values** the program will process and produce.\n",
    "This is a constructive process which helps structure the set of all possible values in meaningful ways\n",
    "and also document the domain upon which programs operate.  \n",
    "\n",
    "As we write more complex programs over more complex data structures - we will feel more strongly the benefit \n",
    "of describing precise data types - which will also guide the structure of the code we write to operate over them.\n",
    "\n",
    "\n",
    "### Types and Set Relations\n",
    "\n",
    "Since types denote set of values, we can define relations among types that are similar to set relations:\n",
    "* Type T1 can be a subset of type T2: this means any value of type T1 is also a value of type T2.  We also say that T1 is a subtype of T2.\n",
    "* Types T1 and T2 can be disjoint - meaning there are no values that are both of type T1 and T2.  For example, \n",
    "`number` and `boolean` are disjoint. \n",
    "* One can define a universal type - which is the type of all possible values.  (This type is exists in TypeScript and is called `any`).\n",
    "* Some types denote finite sets (`boolean` has 2 values), others are infinite (`number`, `string`). \n",
    "* One can construct new types on the basis of existing types: \n",
    "  * The union of T1 and T2 contains all the values of T1 and T2 together.\n",
    "  * The intersection of T1 and T2.\n",
    "  * The cartesian product of T1 and T2 would be the type that contains pairs of values (v1, v2) such that v1 is of type T1 and v2 is of type T2.\n",
    "  \n",
    "This last construction opens the door to compound data types - that is, types which contains values that have sub-components.\n",
    "\n",
    "We will see later that most typed programming languages allow programmers to define new types (user-defined types) on the basis of primitive types (types provided by the language) by using set theory operations like Union, Intersection or Cartesian Product.\n",
    "\n",
    "Different languages offer various levels of introspection (often called *reflection*) to enable the analysis of\n",
    "the type of values *at runtime*, or *at interpretation/compile time*. \n",
    "\n",
    "In JavaScript (the underlying language into which TypeScript is translated), variables are not typed, values have a type (which is encoded in the binary representation of the values in memory) and the `typeof` primitive operator can be used to inspect the type of values at runtime.  Primitives in JavaScript use this introspection mechanism to decide how to operate on each combination of value types they receive as parameters.\n",
    "\n",
    "In contrast, in Java and C/C++, primitive values (non-object values such as integers, booleans, characters, pointers and references) cannot be inspected at runtime: values of different types (for example a char, a boolean or an integer) are encoded in binary format in RAM without any distinctive sign that could be used at runtime to determine that the value belongs to different types."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Types in TypeScript\n",
    "\n",
    "We now describe the basic data types manipulated in TypeScript.\n",
    "The online reference is available at https://www.typescriptlang.org/docs/handbook/basic-types.html \n",
    "\n",
    "TypeScript is a language built on top of JavaScript: it adds optional **type declarations** to variables (which do not exist \n",
    "in JavaScript). The TypeScript compiler (invoked by the command line tool `tsc`) translates TypeScript into JavaScript.\n",
    "During the translation, the TypeScript compiler performs **type checking** - which we will explain later.\n",
    "\n",
    "\n",
    "### Atomic Primitive Value Types\n",
    "\n",
    "Simple values can have the following primitive data types in TypeScript:\n",
    "* Boolean: `true`, `false`;\n",
    "* Number: floating point numbers; `6, 6.1, -4, 0xf0a` (hexadecimal notation)\n",
    "* String: immutable sequences of characters, `\"this is a string\"`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "number\n",
      "boolean\n",
      "string\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "console.log(typeof(6))\n",
    "console.log(typeof(true))\n",
    "console.log(typeof(\"a\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "There are two *special* value types that are not useful on their own - but will play an important role when we start\n",
    "building more complex types:\n",
    "* **null**: this is a type that contains only the special value `null`\n",
    "* **undefined**: this is a type that contains only the special value `undefined`\n",
    "\n",
    "`undefined` plays a special role in the lifecycle of variables.  We will return to this when we discuss the types of\n",
    "variables (as opposed to the type of values which are we now reviewing)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "object\n",
      "undefined\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let null1 = null;\n",
    "let undef = undefined;\n",
    "\n",
    "console.log(typeof(null1));\n",
    "console.log(typeof(undef));"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*NOTE*:\n",
    "*the value of the expression `typeof null` returns `object` - this is a well-known error in JavaScript that\n",
    "has not yet been cleaned up - `null` should still be understood as a distinct atomic primitive value type - not as a compound type.*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Compound Value Types\n",
    "\n",
    "In contrast to atomic values, one can also define *compound values* - which are values that are built from multiple parts.\n",
    "There are two basic compound types in TypeScript:\n",
    "* Arrays\n",
    "* Maps\n",
    "\n",
    "Values of arrays are written as literal constants of the form `[1, 2, 3]`.\n",
    "\n",
    "Maps are written as literal constants of the form: `{ a : 1, b : 2 }`"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Any value that is not an atomic value is a *compound value* - which is called in Javascript an *object* value.\n",
    "\n",
    "*NOTE*:\n",
    "The term of **object** is confusing in this context - it does not refer to *objects* as used in the more standard \n",
    "context of *object oriented programming*.  *Object* in this context means any value which is *not* an atomic value type."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "object\n",
      "object\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let arr1 = [1, 2, 3],\n",
    "    arr2 = ['a', 'b', 'c'];\n",
    "  console.log(typeof(arr1));\n",
    "  console.log(typeof(arr2));"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "object\n",
      "object\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let map1 = { a : 1, b : 2},\n",
    "    map2 = { 'a' : 1, 'b' : 2};\n",
    "  console.log(typeof(map1));\n",
    "  console.log(typeof(map2));"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*NOTE:*\n",
    "Notice that the primitive `typeof` operator is limited in its capability to distinguish the types of values, even if they are \n",
    "very different.  We will see later that TypeScript improves on this operator tremendously.\n",
    "\n",
    "More specific reflection operators allow finer distinction in the types of values, for example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "true\n",
      "false\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let arrIns = [1, 2],\n",
    "    mapIns = { a:1 }\n",
    "  console.log(arrIns instanceof Array);\n",
    "  console.log(mapIns instanceof Array);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Compound values can be entered as constant literals (as above) or can be constructed by invoking the appropriate constructors\n",
    "and mutators (functions which incrementally change a value).\n",
    "\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[ 1, 2, 3 ]"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let arrConstructed = Array(1,2,3)\n",
    "  arrConstructed"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ a: 1, b: 2 }"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let mapConstructed = {}\n",
    "  mapConstructed.a = 1\n",
    "  mapConstructed.b = 2\n",
    "  mapConstructed"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Compound Value Getters\n",
    "\n",
    "Compound values can be \"taken apart\" by using getters - for arrays, using indexes which refer to the positions of the items\n",
    "within the array, and for maps using key values.  In addition, the `slice()` method of arrays can return a range of values from within the array:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "a\n",
      "b\n",
      "[ 'b', 'c', 'd', 'e' ]\n",
      "[ 'b', 'c', 'd' ]\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let arrInd = [\"a\", \"b\", \"c\", \"d\", \"e\"]\n",
    "    console.log(arrInd[0])          // Array indexes start at 0\n",
    "    console.log(arrInd[1])\n",
    "    console.log(arrInd.slice(1))    // Extract from item 1 to the end.\n",
    "    console.log(arrInd.slice(1,4))  // Extract from item 1 to 4 - 4 not included."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Maps are collections of pairs (key, value).\n",
    "\n",
    "Map getters use the key to access the value.\n",
    "\n",
    "Alternatively, the dot notation `m.k` can be used when the key is a string."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1\n",
      "1\n",
      "2\n",
      "2\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let mapInd = { a : 1, b : 2 }   // Note that keys which are strings in key position can skip the quotes - this is the same as { \"a\" : 1, \"b\" : 2}\n",
    "    console.log(mapInd['a'])\n",
    "    console.log(mapInd.a)\n",
    "    console.log(mapInd['b'])\n",
    "    console.log(mapInd.b)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The method `Object.keys(x)` returns the list of the keys which are defined for any compound values.\n",
    "It operates both on arrays (the keys are the indexes) and on maps."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "[ 'a', 'b' ]\n",
      "[ '0', '1', '2' ]\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let mapKey = { a : 1, b : 2},\n",
    "    arrKey = ['a', 'b', 'c'];\n",
    "  console.log(Object.keys(mapKey));\n",
    "  console.log(Object.keys(arrKey));"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Alternatively, one can use the generalized `for` loops over arrays and maps:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "a has value 1\n",
      "b has value 2\n",
      "0 has value a\n",
      "1 has value b\n",
      "2 has value c\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// The backquote notation can be used to generate \"interpolated strings\"\n",
    "// The notation ${expression} in such a string is replaced by the value of the expression converted to a string.\n",
    "for (let k in mapKey) {\n",
    "  console.log(`${k} has value ${mapKey[k]}`);  \n",
    "}\n",
    "for (let i in arrKey) {\n",
    "  console.log(`${i} has value ${arrKey[i]}`);\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Variable Types in TypeScript: Gradual Typing\n",
    "\n",
    "In *static languages* like C++ and Java, variables must be typed - that is, when a variable is defined, its type must be declared by the programmer. \n",
    "\n",
    "In *dynamically typed languages* like JavaScript and Scheme, variables are not typed.  \n",
    "But when a variable is bound to a value, we can inspect its type at runtime (because values are always typed).\n",
    "\n",
    "TypeScript extends JavaScript and introduces *optional variable types*.\n",
    "TypeScript is compiled into JavaScript - and at compilation time, type checking is performed.\n",
    "There is no additional type checking happening at runtime after compilation has completed.\n",
    "\n",
    "Typing annotations can be introduced gradually as code matures.\n",
    "(See https://en.wikipedia.org/wiki/Gradual_typing).\n",
    "\n",
    "Typing a variable means that the programmer declares how she intends to use the variable - which values it can be bound to.\n",
    "In TypeScript, this is performed by adding a type annotation to variable declarations:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "let typedVarNum  : number = 6,\n",
    "    typedVarStr  : string = \"blue\",\n",
    "    typedVarBool : boolean = true;"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Summary\n",
    "\n",
    "### Concepts\n",
    "* Programming Language *semantics* defines the requirements for tools that manipulate programs: interpreters, compilers, debuggers etc.  It helps determine whether 2 programs are equivalent.\n",
    "* The *Operational Semantics* of programming language defines the meaning of programs by mapping programs to evaluation histories. \n",
    "* *Operational semantics* provide recursive *evaluation rules* for each specific syntactic construct in a programming language.\n",
    "\n",
    "* *Expressions* in an FP language are computed into *values*. This process can be described as *reduction*.\n",
    "\n",
    "* *Runtime errors* can be triggered when parameters of the wrong type are passed to primitives (in Scheme) or when undefined variables are accessed.\n",
    "* *Type safety* guarantees at compile time that a well-typed program will not lead to type runtime errors. It requires that the compiler determines the type of variables - which means to which types of values the variable can ever be bound.\n",
    "\n",
    "* *Data types* are defined by 2 aspects: they are *sets of values* and they determine which *operations can be used on values*.\n",
    "* *Values* can be *atomic* (no sub-part) or *compound* (made up of multiple parts).\n",
    "\n",
    "* TypeScript adds the option of *gradual typing* on top of JavaScript\n",
    "* *Primitive atomic types* in TypeScript are *number*, *boolean*, *string*, *undefined* and *null*.\n",
    "* *Primitive compound types* in TypeScript are *array* and *map*.\n",
    "\n",
    "### Compound Types Operations\n",
    "* Literal constants for arrays are written as `[1, 2, 3]`\n",
    "* Literal constants for maps are written as `{ k1 : 1, k2 : 2}`\n",
    "* Parts of an array are accessed using number indexes starting with 0: `arr[0], arr[1]`\n",
    "* Parts of a map are accessed using key indexes: `map[k1]` or the dot notation `map.k1`\n",
    "* The list of indexes that can be used to access parts of a compound values is returned by `Object.keys(value)`\n",
    "  or using the construct `for (let k in object) { ... }`.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "kernelspec": {
   "display_name": "Typescript 2.9",
   "language": "typescript",
   "name": "typescript"
  },
  "language_info": {
   "file_extension": ".ts",
   "mimetype": "text/x-typescript",
   "name": "typescript",
   "version": "2.9.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}

